i, j:. (i <z j = ff  )  ((i < j)) 

latex

ProofTree

Definitions	, t  T, P  Q, x:A. B(x), P  Q, P & Q, T, P  Q, False, A, True, A  B
Lemmas	bfalse wf, lt int wf, bool wf, assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, iff transitivity, bnot wf, le wf, le int wf, assert wf